Nuprl Lemma : R-sends-rule
11,40
postcript
pdf
k
:Knd,
T
:Type,
l
:IdLnk,
ds
,
dt
:fpf(Id;
tg
.Type),
g
:((
tg
:Id
(decl-state(
ds
)
T
(decl-type{i:l}(
dt
;
tg
) List))) List).
((
isrcv(
k
))
((destination(lnk(
k
)) = source(
l
)
Id)
((
eq_lnk(lnk(
k
);
l
))
(
T
= decl-type{i:l}(
dt
; tag(
k
))))))
normal-ds{i:l}
normal-ds
(
ds
)
normal-type{i:l}
normal-type
(
T
)
normal-ds{i:l}
normal-ds
(
dt
)
R-realizes{i:l}
R-realizes
(Rsends(
ds
;
k
;
T
;
l
;
dt
;
g
);
es
.sends-p(
es
;
ds
;
k
;
T
;
l
;
dt
;
g
))
latex
Definitions
x
.
t
(
x
)
,
prop{i:l}
,
t
T
,
A
c
B
,
R-Feasible{i:l}(
R
)
,
R-realizes{i:l}(
R
;
es
.
P
(
es
))
,
P
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
x
(
s
)
,
R-consistent(
R
;
es
)
,
normal-type{i:l}(
T
)
,
normal-ds{i:l}(
ds
)
,
decl-type{i:l}(
ds
;
x
)
Lemmas
Knd
wf
,
IdLnk
wf
,
fpf
wf
,
decl-state
wf
,
tagof
wf
,
decl-type
wf
,
lsrc
wf
,
ldst
wf
,
Id
wf
,
isrcv
wf
,
normal-type
wf
,
normal-ds
wf
,
event
system
wf
,
Rsends
wf
,
R-consistent
wf
,
lnk
wf
,
eq
lnk
wf
,
assert
wf
origin